00100 P(X1 G(X1) E); 00200 P(X1 E X1); 00300 ¬P(X1 X2 X3) ∨ ¬P(X2 X4 X5) ∨ ¬P(X1 X5 X6) ∨ P(X3 X4 X6); 00400 ¬P(X1 X2 X3) ∨ ¬P(X2 X4 X5) ∨ ¬P(X3 X4 X6) ∨ P(X1 X5 X6); 00500 ; 00600 ; 00700 ∀(X1)∃(X2)P(X2 X1 E); 00800 ;